FR.LSP[BNF,JRA] - www.SailDart.org

perm filename FR.LSP[BNF,JRA] blob sn#045428 filedate 1973-05-24 generic text, type T, neo UTF8

(DEFPROP <AXIOM> 
 (LAMBDA NIL
  (NLRR (QUOTE AXIOM)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<NAME>) (<ASSUM>) (<DRECUR>) (<INEQ>) (<BODY>))
		 (PROG (LSTNAME)
		       (SETQ LSTNAME (READLIST (APPEND LST (EXPLODE (STK4)))))
		       (RETURN
			(LIST (QUOTE DEFPROP)
			      (STK4)
			      (CONS (QUOTE THCONSE)
				    (CONS (APPEND (UNION POSTLIST PRELIST)
						  (LIST (QUOTE CGL)
							(LIST LSTNAME (LIST (QUOTE QUOTE) POSTLIST))))
					  (APPEND (CDR (STK0))
						  (QUOTE ((THSETQ (THV LCTR) (THV GCTR))))
						  (COND ((NULL (STK2)) (LIST (LIST (QUOTE THUNIQUE) LSTNAME))))
						  (LIST (LIST (QUOTE TREEPATH) (STK4) (CADR (STK0)))
							(QUOTE (TRACEINFO1))
							(LIST (QUOTE THOR) T (LIST (QUOTE TRACEINFO2) (STK4)))
							(QUOTE (COND ((TTYIN) (ADVICESYS)))))
						  (COND
						   ((EQ (CAAR (STK0)) (QUOTE THAND)) (CDAR (STK0)))
						   (T (LIST (CAR (STK0)))))
						  (QUOTE
						   ((THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
						    (COND
						     ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE))
						     (T (THSETQ CT (CDR CT) T T))))))))
			      (QUOTE THEOREM)))))
		(*NIL*)))))) 
EXPR)

(DEFPROP <NAME> 
 (LAMBDA NIL
  (NLRR (QUOTE NAME)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<ID>)) (PROG2 (SETQ VARLIST (SETQ POSTLIST (SETQ PRELIST NIL))) (STK0))) (*NIL*)))))) 
EXPR)

(DEFPROP <ASSUM> 
 (LAMBDA NIL
  (NLRR (QUOTE ASSUM)
	(FUNCTION (LAMBDA NIL (COND ((AND (SPWD T)) (QUOTE T)) ((AND (SPWD NIL)) NIL) (*NIL*)))))) 
EXPR)

(DEFPROP <DRECUR> 
 (LAMBDA NIL
  (NLRR (QUOTE DRECUR)
	(FUNCTION (LAMBDA NIL (COND ((AND (SPWD T)) (QUOTE T)) ((AND (SPWD NIL)) NIL) (*NIL*)))))) 
EXPR)

(DEFPROP <INEQ> 
 (LAMBDA NIL
  (NLRR (QUOTE INEQ)
	(FUNCTION (LAMBDA NIL (COND ((AND (SPWD NIL)) NIL) ((AND (CH /() (<INARGS>)) (STK 0)) (*NIL*)))))) 
EXPR)

(DEFPROP <INARGS> 
 (LAMBDA NIL
  (NLRR (QUOTE INARGS)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<INARG>) (CH /,) (<INARGS>)) (CONS (STK 2) (STK 0)))
		((AND (<INARG>) (CH /))) (CONS (STK 1) NIL))
		(*NIL*)))))) 
EXPR)

(DEFPROP <INARG> 
 (LAMBDA NIL
  (NLRR (QUOTE INARG)
	(FUNCTION (LAMBDA NIL (COND ((AND (SPWD X)) (QUOTE X)) ((AND (CH ⊗)) (QUOTE ⊗)) (*NIL*)))))) 
EXPR)

(DEFPROP <BODY> 
 (LAMBDA NIL
  (NLRR (QUOTE BODY)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<PRECONDS>) (<POSTCOND>)) (PROG2 (SETQ POSTLIST VARLIST) (CONS (STK1) (STK0))))
		(*NIL*)))))) 
EXPR)

(DEFPROP <PRECONDS> 
 (LAMBDA NIL
  (NLRR (QUOTE PRECONDS)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<PC>) (CH ;)) (PROG NIL (SETQ PRELIST VARLIST) (SETQ VARLIST NIL) (RETURN (STK1))))
		(*NIL*)))))) 
EXPR)

(DEFPROP <PC> 
 (LAMBDA NIL
  (NLRR (QUOTE PC)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<C1>) (<PCL>)) (CONS (QUOTE THAND) (CONS (STK1) (STK0))))
		((AND (<C1>)) (STK 0))
		(*NIL*)))))) 
EXPR)

(DEFPROP <PCL> 
 (LAMBDA NIL
  (NLRR (QUOTE PCL)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<C1>) (<PCL>)) (CONS (STK 1) (STK 0))) ((AND (<C1>)) (CONS (STK 0) NIL)) (*NIL*)))))) 
EXPR)

(DEFPROP <C1> 
 (LAMBDA NIL (NLRR (QUOTE C1) (FUNCTION (LAMBDA NIL (COND ((AND (<C>) (CH ;)) (STK 1)) (*NIL*)))))) 
EXPR)

(DEFPROP <C> 
 (LAMBDA NIL
  (NLRR (QUOTE C)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<PRED>) (<CL>))
		 (APPEND (CONS (QUOTE THOR) (CONS (STK1) (STK0))) (QUOTE ((CONDSTAT (THV GCL) T)))))
		((AND (<PRED>)) (STK 0))
		((AND (CH /() (<PC>) (CH /))) (STK 1))
		(*NIL*)))))) 
EXPR)

(DEFPROP <CL> 
 (LAMBDA NIL
  (NLRR (QUOTE CL)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<PRED>) (<CL>)) (CONS (STK 1) (STK 0)))
		((AND (<PRED>)) (CONS (STK 0) NIL))
		((AND (CH /() (<PC>) (CH /))) (CONS (STK 1) NIL))
		(*NIL*)))))) 
EXPR)

(DEFPROP <PRED> 
 (LAMBDA NIL
  (NLRR (QUOTE PRED)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<NOT>) (<LIT>))
		 (COND ((EQ (CAR (STK0)) (QUOTE =)) (MAKEQUAL (CDR (STK0)) (CONS (QUOTE EQUAL) (CDR STK0))))
		       (T (MAKENOT (STK0)))))
		((AND (<LIT>))
		 (COND ((EQ (CAR (STK0)) (QUOTE =))
			(MAKEQUAL (CDR (STK0)) (LIST (QUOTE NOT) (CONS (QUOTE EQUAL) (CDR (STK0))))))
		       (T (MAKEPRED (STK0)))))
		(*NIL*)))))) 
EXPR)

(DEFPROP <LIT> 
 (LAMBDA NIL
  (NLRR (QUOTE LIT)
	(FUNCTION (LAMBDA NIL (COND ((AND (<PREDLET>) (<ITMLST>)) (CONS (STK 1) (STK 0))) (*NIL*)))))) 
EXPR)

(DEFPROP <ITMLST> 
 (LAMBDA NIL (NLRR (QUOTE ITMLST) (FUNCTION (LAMBDA NIL (COND ((AND (CH /() (<ITMS>)) (STK 0)) (*NIL*)))))) 
EXPR)

(DEFPROP <ITMS> 
 (LAMBDA NIL
  (NLRR (QUOTE ITMS)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<TM2>) (<ITMS>)) (CONS (STK 1) (STK 0)))
		((AND (<TM>) (CH /))) (CONS (STK 1) NIL))
		(*NIL*)))))) 
EXPR)

(DEFPROP <TM2> 
 (LAMBDA NIL (NLRR (QUOTE TM2) (FUNCTION (LAMBDA NIL (COND ((AND (<TM>) (CH /,)) (STK 1)) (*NIL*)))))) 
EXPR)

(DEFPROP <TM> 
 (LAMBDA NIL
  (NLRR (QUOTE TM)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<IVAR>))
		 (PROG2 (COND ((NOT (MEMQ (STK0) VARLIST)) (SETQ VARLIST (CONS (STK0) VARLIST))))
			(LIST (QUOTE THV) (STK0))))
		((AND (<PREFN>) (<ITMLST>)) (CONS (STK 1) (STK 0)))
		((AND (<PREFN>)) (CONS (STK 0) NIL))
		(*NIL*)))))) 
EXPR)

(DEFPROP <POSTCOND> 
 (LAMBDA NIL
  (NLRR (QUOTE POSTCOND)
	(FUNCTION
	 (LAMBDA NIL
	  (COND ((AND (<POSTPRED>) (CH ;) (<POSTCOND>)) (CONS (STK 2) (STK 0))) ((AND (CH ;)) NIL) (*NIL*)))))) 
EXPR)

(DEFPROP <POSTPRED> 
 (LAMBDA NIL
  (NLRR (QUOTE POSTPRED)
	(FUNCTION
	 (LAMBDA NIL (COND ((AND (<NOT>) (<LIT>)) (CONS (STK 1) (STK 0))) ((AND (<LIT>)) (STK 0)) (*NIL*)))))) 
EXPR)

(DEFPROP <IVAR> 
 (LAMBDA NIL (NLRR (QUOTE IVAR) (FUNCTION (LAMBDA NIL (COND ((AND (<ID>)) (STK 0)) (*NIL*)))))) 
EXPR)

(DEFPROP <PREFN> 
 (LAMBDA NIL (NLRR (QUOTE PREFN) (FUNCTION (LAMBDA NIL (COND ((AND (<ID>)) (STK 0)) (*NIL*)))))) 
EXPR)

(DEFPROP <PREDLET> 
 (LAMBDA NIL
  (NLRR (QUOTE PREDLET)
	(FUNCTION (LAMBDA NIL (COND ((AND (<ID>)) (STK 0)) ((AND (CH =)) (QUOTE =)) (*NIL*)))))) 
EXPR)

(DEFPROP <NOT> 
 (LAMBDA NIL (NLRR (QUOTE NOT) (FUNCTION (LAMBDA NIL (COND ((AND (CH ¬)) (QUOTE ¬)) (*NIL*)))))) 
EXPR)